1. Field of the Invention
The present invention relates to digital circuitry designs of state machines, and more specifically, to systems, methods and computer products for efficiency improvements in the digital circuitry designs.
2. Description of Related Art
An electrical circuit with memory elements may be modeled using state equations and state variables to describe the behavior and state of the system. A complete set of state variables for a system, coupled with logic that defines the transitions between states, typically contains enough information about the system's history to enable computation of the system's future behavior. Simplifying the model to reduce the number of state variables, or simplifying the logic that defines state transitions, lessens the computational cost of analyzing the model. A simplified model should be subjected to verification analysis to verify its equivalence to the original circuit model.
Many conventional verification proof algorithms rely upon reachability analysis, which requires enumerating the reachable states of the design under test to assess whether the design conforms to its specification, which unfortunately is a size-limited process. Certain gates of the model may be labeled as targets. Targets correlate to the properties we wish to verify. One goal of the verification process is to find a way to drive a “1” to a target node, or to prove that no such assertion of the target is possible—that is, to verify whether or not the target node is reachable.
Reachability analysis can identify whether a proposed design satisfies its specification. If all reachable states of a design satisfy the property being verified, then a correctness proof has been completed and the proposed design is known to satisfy its specification. Reachability analysis can also identify whether the design does not satisfy its specification if it is determined that some reachable state does not satisfy the property being verified. Symbolic space traversal using Binary Decision Diagrams (BDD) is a well established technique in reachability analysis. The breadth-first traversal starts from the initial states and computes all the reachable states in one time step and represents all the reached states (including the initial states) using a BDD. If there are new states reached in that image computation then in subsequent steps states that are reachable from the newly reached states will be explored. This process of reachability analysis will eventually converge since the state space being searched in the hardware design is normally finite.
The powerful technique of reachability analysis has one Achilles heel, that is—the state explosion we might encounter during the image computation. The intermediate BDD that represent a set of reachable states at kth depth can have such a large representation and push the computation above its memory resource. Techniques have been proposed to overcome this state explosion problem caused by the intermediate BDDs. For example, applying hints to guide the state exploration is one of the effective techniques that create opportunities to overcome the computational bottleneck of representing monstrous intermediate BDDs, as described in “Hints to accelerate Symbolic Traversal” by Kavita Ravi and Fabio Somenzi CHARME 1999, pp. 250-264. Hints are constraints on the transition relation of the circuit being verified. Hints are expressed as constraints on the primary inputs and the states of a circuit which is modeled as a finite transition system. During the reachability analysis a set of hints are applied in sequence, and the final converged reachable states of one hint application will be served as the initial state of the next hint application, with the last hint to be the constant 1, which indicates that it offers no constraining power on the transition relation.
Conventional systems generate hints manually with the help of simple heuristics by someone who understands the circuit well enough to devise simulation stimuli or verification properties for it. However, finding good hints requires one to constrain the transition system in such a way that only small intermediate BDDs arise during image computations that produce large numbers of reachable states. The practice of finding good hints is limited by the user's ability to predict their usefulness, often requiring a significant amount of manual trial-and-error.
Another effort in the automatic hints generation is that of Somenzi and Ward as described in “Automatic Generation of Hints for Symbolic Traversal,” CHARME 2005; pps. 207-221. Somenzi and Ward present a method intended to statically and automatically determine good hints. Working on the control flow graph(s) of a behavioral model of the circuit being analyzed, their algorithm extracts sets of related execution paths each corresponds to enabling predicates which trigger various control flow paths as a candidate hint. However, that approach requires a very specific design representation to be able to work—namely, a behavioral hardware description languages (HDL) model. In practice, such models tend not to be available because high-performance hardware designs (e.g. multi-gigahertz) are pipelined to the extent that behavioral representations are not available whatsoever; even control flows are pipelined in the source HDL. Further, formal verification often requires preprocessing using bit-level design optimization techniques prior to BDD-based reachability, e.g., retiming and redundancy removal. Such transformations require a synthesized bit-level model of a design, and produce the same. Various embodiments of the present invention eliminate both of these limitations by operating directly on a bit-level synthesized netlist.
What is needed is an improved system for automatically generating and applying hints to aid in the reachability analysis for verifying improved circuitry designs.